E:Type{i}, T, V:(IdIdType{i}), M:(IdLnkIdType{i}), loc:(EId), kind:(EKnd),
val:(e:Eeventtype(kind;loc;V;M;e)), when, after:(x:Ide:ET(loc(e),x)),
sends:(l:IdLnkE(Msg_sub(l;M) List)), sender:({e:E| isrcv(kind(e)) }E),
index:(e:{e:E| isrcv(kind(e)) }||sends(lnk(kind(e)),sender(e))||), first:(E),
pred:({e':E| first(e') }E), causl:(EEProp{i}).
ESAxioms{i:l}
ESAxioms(E; T; M; loc; kind; val; when; after; sends; sender; index; first; pred; causl)
 Prop{i'} 

latex

Definitions

x:A. B(x), Prop, t  T, ESAxioms(E;T;M;loc;kind;val;when;after;sends;sender;index;first;pred;causl), P & Q, P  Q, P  Q, P  Q, A & B, x:A. B(x), P  Q, x,y. t(x;y), S  T, T, True, eventtype(k;loc;V;M;e), b, isrcv(k), lnk(k), tag(k), kindcase(k; a.f(a); l,t.g(l;t) ), isl(x), 1of(t), outl(x), if b t else f fi, islocal(k), act(k), 2of(t), true, false, b, outr(x), Msg_sub(l;M), {i..j}, x(s1,s2), SqStable(P), Knd, False, locl(a), rcv(l,tg)

Lemmas

iff wf, assert wf, not wf, trans wf, strongwellfounded wf, isrcv wf, Msg wf, select wf, lnk wf, Msg sub wf, int seg wf, length wf1, non neg length, msg wf, tagof wf, ldst wf, lsrc wf, bool wf, sq stable from decidable, decidable assert, IdLnk wf, Id wf, eventtype wf, Knd wf, subtype rel self, true wf, false wf